Inference at * 1 3 
Iof proof for Lemma quotient wf:

.....eq aux..... NILNIL

1. T : Type
2. E : TT
3. (a:T. E(a,a)) & (a, b:T. E(a,b)  E(b,a)) & (a, b, c:T. E(a,b)  E(b,c)  E(a,c))
4. x : T
5. y : T
6. x1 : T
7. E(x,y)
8. E(y,x1)
  E(x,x1) 

latex

 by RepD 

latex

 1: 

 1: 3. a:T. E(a,a)
 1: 4. a, b:T. E(a,b)  E(b,a)
 1: 5. a, b, c:T. E(a,b)  E(b,c)  E(a,c)
 1: 6. x : T
 1: 7. y : T
 1: 8. x1 : T
 1: 9. E(x,y)
 1: 10. E(y,x1)
 1:   E(x,x1)
 .

Definitions

P & Q